#!/usr/bin/env python
#-*- coding:utf-8 -*-

from z3 import *


f=open("/Users/hellok/Downloads/wikipedia-wordlist-sraveau-20090325.txt")
length = 6

def loop(x,c):
    return x + c + (x << 6) + (x << 16)

x = BitVecVal(0,32)

S = [ BitVec('s%s' % i, 32)for i in xrange(length) ]
for i in xrange(length):
    x = loop(x, S[i])

solver = Solver()
#solver.add(x == 0x38B7E73C) 19 #solver.add(x == 0x991181AE)
solver.add(x == 0x478692F9)
for i in xrange(length):
    solver.add(S[i] < 128, S[i] >= 32)
print solver.check()
m = solver.model()
string = ''
for i in xrange(length):
    string += chr(int('%s' % (m[S[i]])))
print string

for line in f:
    acc = 0
    line = line.strip()
    for c in line:
        acc = (acc + ord(c) + (acc << 6) + (acc << 16)) & 0xFFFFFFFF
    if (acc == 0x38B7E73C): # Change this
        print line
